Inference at * 1 2 3 
Iof proof for Lemma append overlapping sublists:

.....wf..... NILNIL

1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
15. f2 : {0..||L1 @ [x / L2]||}{0..||L||}
  (increasing(f2;||L1 @ [x / L2]||)
  (& (j:{0..||L1 @ [x / L2]||}. (L1 @ [x / L2])[j] = L[(f2(j))]))
    

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)
 b

latex

 .

Definitions	suptype(S; T), S  T, False, A  B, Y, t  ...$L, P & Q, , t  T, i  j , A, ||as||, P  Q, x:A. B(x), {i..j}
Lemmas	select wf, length wf1, int seg wf, length append, append wf, length nil, non neg length, length cons, increasing wf